00100	(DE CHOICE (X)(PROG(Z Z1 Z2)
00110	(COND((NOT(HERE X))(RETURN NIL))
00120	   (ANCESTRY(SETQ Z(CHOICE1 X LLST)))
00130	(T(SETQ Z CLAUSES)))
00140	A(SETQ Z1(CAR Z))
00150	(COND((OR (NOT(HERE Z1))
00160	    (AND PFLG(ALLPOS X)(ALLPOS Z1))
00170	 (AND(ALLNEG Z1)(ALLNEG X))
00180	 (AND STRATEGY (NOT(STRATEGY X Z1)))) NIL)
00190	(T(SETQ Z2(NCONC Z2(LIST Z1)))) )
00200	(SETQ Z(CDR Z))
00210	(COND((OR (EQ Z X)(NULL Z))(RETURN Z2)))
00220	(GO A) ))
00230	
00300	(DEFPROP TRYIT 
00400	 (LAMBDA NIL
00500	  (PROG (Z1 Z2 R M)
00600		(SETQ CNT (ADD1 (LENGTH CLAUSES)))
00700		(SETQ EE (CDR EE))
00800	   TRY3 (SETQ Z1 (CAR EE))
00900		(COND ((NOT (HERE Z1)) (GO TRY7)))
01000		(SETQ M (CHOICE Z1 ))
01100		(COND ((NULL M) (GO TRY7)))
01200	   TRY2 (SETQ Z2 (CAR M))
01300		(COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
01400	   TRY1 TRY1A
01500		(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)))
01600		(SETQ R (RESOLVE Z1 Z2))
01700		(COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
01800		(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
02000	   TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
02100		(SETQ R (PARMOD Z1 Z2))
02200		(COND ((NULL R) (GO TRY8)))
02300		(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
02500	   TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
02600		(SETQ M (CDR M))
02700		(COND (M (GO TRY2)))
02800	   TRY7 (SETQ EE (CDR EE))
02900		(COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
03100		(PRINT (QUOTE COUNT))
03200		(PRINT COUNT)
03300		(PRINT (QUOTE LEVEL))
03400		(PRINT LVL)
03500		(SETQ LVL (ADD1 LVL))
03600		(PRINT (QUOTE ELAPSED-TIME))
03700		(PRINT (TIMEIT))
03800		(COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
03900		(PRINT (QUOTE NO-PROOF-FOUND))
04000		(COND (AUTO (ERR (QUOTE NOPROOF))))
04100		(UPDATE CLAUSES)
04200		(COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
04300		(ERR (QUOTE NOPROOF)))) 
04400	EXPR)
04500	
04600	(DEFPROP ATTEMPT 
04700	 (LAMBDA(Z S C)
04800	  (PROG (NEWNAME SUPPORT
04900	 		 EDITSTRAT
05000	 		 LCL
05100	 		 LVL
05200	 		 CNT
05400	 		 LSTCLS
05500	 		 LLST
05600	 		 Z1
05700	 		 MERGE
05800	 		 ORDER
05900	 		 DEBUG
06000	 		 DEPTH
06100	 		 LENGTH
06200	 		 ANCESTRY
06300	 		 STRATEGY
06400	 		 STRAT
06500	 		 PMODEL
06600	 		 NMODEL
06700	 		 PFLG
06800	 		 PDEPTH
06900	 		 DLIST
07000	 		 XYZ
07100	 		 XYZ1
07200	 		 COND
07300	 		 UNAXP
07400	 		 UNAXN
07500	 		 SAT
07600	 		 EE
07700	 		 EE1
07900	 		 CLAUSES
08000	 		 SUBCLAUSES
08100	 		 COUNT)
08200		(SETQ TBL (SET1 (APPEND PREFN INFN)))
08300		(SET3 Z)
08400		(SETQ Z (MINIMIZE Z))
08500		(SETQ NEWNAME (INITIAL Z))
08550	(SETQ CLAUSES Z)
08600		(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
08700		(SETQ COND C)
08900		(SETQ LVL 1)
09000		(SETQ COUNT 0)
09100		(SETQ Z (UNITPN Z))
09200		(SETQ UNAXP (CAR Z))
09300		(SETQ UNAXN (CDR Z))
09500		(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
09600				  (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
09700		      (T (SETQ SUBCLAUSES CLAUSES)))
09800		(SETQ LCL (LAST CLAUSES))
09900		(SETQ LSTCLS LCL)
10000	(SETQ XYZ(SETQ EE CLAUSES))(SETQ EE1(LAST CLAUSES))
10100	BB(SETQ LLST(CONS(CAR XYZ)LLST))
10200	(SETQ XYZ(CDR XYZ))(COND(XYZ(GO BB)))
10300	(SETQ Z1(ERRSET(TRYIT)))
10600		(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
10700		      ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
10800						       (EVAL
10900							(LIST (QUOTE OUTC)
11000							      (LIST (QUOTE OUTPUT)
11100								    (QUOTE PRF)
11200								    (QUOTE DSK:)
11300								    (CONS (READLIST
11400									   (CONS (QUOTE N)
11500										 (CONS (SETQ PRNO (ADD1 PRNO))
11600	 									       FILENAM)))
11700									  (QUOTE PRF)))
11800	 						      NIL)))
11900						 (QUERY)
12000						 (PROOF LHP RHP)
12100						 (OUTC Z T)
12200						 (RETURN Z1))
12300		      (T (RETURN Z1)))
12400	))
13000	EXPR)